(set-logic BV)
(synth-fun f ( (x (BitVec 64)) ) (BitVec 64)
((Start (BitVec 64)
((bvnot Start)
(bvxor Start Start)
(bvand Start Start)
(bvor Start Start)
(bvneg Start)
(bvadd Start Start)
(bvmul Start Start)
(bvudiv Start Start)
(bvurem Start Start)
(bvlshr Start Start)
(bvashr Start Start)
(bvshl Start Start)
(bvsdiv Start Start)
(bvsrem Start Start)
(bvsub Start Start)
x
#x0000000000000000
#x0000000000000001
#x0000000000000002
#x0000000000000003
#x0000000000000004
#x0000000000000005
#x0000000000000006
#x0000000000000007
#x0000000000000008
#x0000000000000009
#x0000000000000009
#x0000000000000009
#x000000000000000A
#x000000000000000B
#x000000000000000C
#x000000000000000D
#x000000000000000E
#x000000000000000F
#x0000000000000010
(ite StartBool Start Start)
))
(StartBool Bool
((= Start Start)
(not StartBool)
(and StartBool StartBool)
(or StartBool StartBool)
))))
(constraint (= (f #xe6d77a0b5e99de57) #xcdaef416bd33bcae))
(constraint (= (f #xebe894a3e2de3566) #xebe894a3e2de3566))
(constraint (= (f #x332338569521ac90) #x664670ad2a435920))
(constraint (= (f #x1ee8d67430c55e5e) #x3dd1ace8618abcbc))
(constraint (= (f #xdd074508cc76db9b) #xba0e8a1198edb736))
(constraint (= (f #x9e60e52e72c0e16d) #x9e60e52e72c0e16d))
(constraint (= (f #x34d793a28a224002) #x69af274514448004))
(constraint (= (f #xcab334873b438eb5) #x0000000000000001))
(constraint (= (f #xe8846ca8bc5e3579) #xe8846ca8bc5e3579))
(constraint (= (f #x05badaba2b88e35b) #x0b75b5745711c6b6))
(constraint (= (f #x475c2e1d6ad3914a) #x8eb85c3ad5a72294))
(constraint (= (f #xa424e38201bc91ee) #xa424e38201bc91ee))
(constraint (= (f #x9e99eeabee65b650) #x3d33dd57dccb6ca0))
(constraint (= (f #xa07ecd2c24072383) #x40fd9a58480e4706))
(constraint (= (f #x6dee117e45445dc3) #xdbdc22fc8a88bb86))
(constraint (= (f #xd0e071ce2ad99210) #xa1c0e39c55b32420))
(constraint (= (f #x38b17ae6aca68a83) #x7162f5cd594d1506))
(constraint (= (f #x8559ce836d3a579e) #x0ab39d06da74af3c))
(constraint (= (f #xc8d54663a0ece523) #xc8d54663a0ece523))
(constraint (= (f #xa9ece36322894838) #x0000000000000000))
(constraint (= (f #x3010965e58290be4) #x0000000000000000))
(constraint (= (f #xe463e6b837d0e9ee) #xe463e6b837d0e9ee))
(constraint (= (f #x6ac6b364eac124e3) #x0000000000000001))
(constraint (= (f #xc8a3e3d7d18cd417) #x9147c7afa319a82e))
(constraint (= (f #x9ce4e557c6d59e01) #x39c9caaf8dab3c02))
(constraint (= (f #xec039a0148b3a43d) #x0000000000000001))
(constraint (= (f #x7983484a6cbc3b46) #xf3069094d978768c))
(constraint (= (f #xded4eee3e4e700c1) #xbda9ddc7c9ce0182))
(constraint (= (f #x2c4c2b30a36c801e) #x5898566146d9003c))
(constraint (= (f #x1e9768665c102e49) #x3d2ed0ccb8205c92))
(constraint (= (f #x8613d6120a00549a) #x0c27ac241400a934))
(constraint (= (f #xe08aba8e08e5e386) #xc115751c11cbc70c))
(constraint (= (f #x2e58e0a362a94a94) #x5cb1c146c5529528))
(constraint (= (f #xe914ae30ebd2a812) #xd2295c61d7a55024))
(constraint (= (f #xd990517946804688) #xb320a2f28d008d10))
(constraint (= (f #xbe0ad22511c14a28) #x0000000000000000))
(constraint (= (f #x3e4d4d78e5693a51) #x7c9a9af1cad274a2))
(constraint (= (f #xea5ce7a144cd2151) #xd4b9cf42899a42a2))
(constraint (= (f #xa707e257425c1498) #x4e0fc4ae84b82930))
(constraint (= (f #x8c6b42a85346206e) #x8c6b42a85346206e))
(constraint (= (f #x19ee083e891eb834) #x19ee083e891eb834))
(constraint (= (f #xce893d66c102c3d0) #x9d127acd820587a0))
(constraint (= (f #xa0bc9b62e634918d) #x417936c5cc69231a))
(constraint (= (f #xa4ea5a541e12440c) #x49d4b4a83c248818))
(constraint (= (f #x29371eec9c91518d) #x526e3dd93922a31a))
(constraint (= (f #xcee356187d77475e) #x9dc6ac30faee8ebc))
(constraint (= (f #xa48eac98e29e4e3d) #xa48eac98e29e4e3d))
(constraint (= (f #x8dc6562732e8c6c2) #x1b8cac4e65d18d84))
(constraint (= (f #xe40e6483b25aa504) #xc81cc90764b54a08))
(constraint (= (f #xa8b8abe8b92cc0be) #xa8b8abe8b92cc0be))
(constraint (= (f #x9be042293a6bed73) #x0000000000000001))
(constraint (= (f #xbd1c7906ede2ec18) #x7a38f20ddbc5d830))
(constraint (= (f #x6de1b58aad465339) #x6de1b58aad465339))
(constraint (= (f #x8edb8833934e6a24) #x8edb8833934e6a24))
(constraint (= (f #x9ec64e1b32627ae8) #x9ec64e1b32627ae8))
(constraint (= (f #xa5e7d5d09251e4e4) #x0000000000000000))
(constraint (= (f #xa2d6ea202bde61c9) #x45add44057bcc392))
(constraint (= (f #xe19bd818e71be11e) #xc337b031ce37c23c))
(constraint (= (f #x808e502366b14418) #x011ca046cd628830))
(constraint (= (f #x299332339e575513) #x532664673caeaa26))
(constraint (= (f #x002e1037d4a879c5) #x005c206fa950f38a))
(constraint (= (f #x5511790825d89e53) #xaa22f2104bb13ca6))
(constraint (= (f #x166194a2b7ada48b) #x2cc329456f5b4916))
(constraint (= (f #x7bca3abe346c3059) #xf794757c68d860b2))
(constraint (= (f #xb852ce0deae0b18d) #x70a59c1bd5c1631a))
(constraint (= (f #x246d07a282cb3070) #x0000000000000000))
(constraint (= (f #xe0e95ed8039a1165) #xe0e95ed8039a1165))
(constraint (= (f #x39e47e46b9389228) #x39e47e46b9389228))
(constraint (= (f #x19bd70a1780315c4) #x337ae142f0062b88))
(constraint (= (f #x6de1ed8dce87a4ed) #x0000000000000001))
(constraint (= (f #xd71ba1a09ac832e4) #xd71ba1a09ac832e4))
(constraint (= (f #x868c4db9e8c476bb) #x868c4db9e8c476bb))
(constraint (= (f #x468eebc02a4b860d) #x8d1dd78054970c1a))
(constraint (= (f #x5bb4863be8633dcb) #xb7690c77d0c67b96))
(constraint (= (f #xdbaacce9ee59c390) #xb75599d3dcb38720))
(constraint (= (f #xce3036d922a8d9e9) #xce3036d922a8d9e9))
(constraint (= (f #x34bbce2c611610b6) #x34bbce2c611610b6))
(constraint (= (f #x5deb0aea3570aae2) #x5deb0aea3570aae2))
(constraint (= (f #xc18ed30033d534bd) #x0000000000000001))
(constraint (= (f #xcdc3d7e45222821a) #x9b87afc8a4450434))
(constraint (= (f #x9bab2d4075dababe) #x9bab2d4075dababe))
(constraint (= (f #x7a0ec70ab148b30d) #xf41d8e156291661a))
(constraint (= (f #x04e5e488461c881c) #x09cbc9108c391038))
(constraint (= (f #x791ceed8ee753c63) #x0000000000000001))
(constraint (= (f #x7be4dc5d635db41e) #xf7c9b8bac6bb683c))
(constraint (= (f #x3ed794ec25d130b1) #x0000000000000001))
(constraint (= (f #xc751e4269e7788c9) #x8ea3c84d3cef1192))
(constraint (= (f #x762e6e641e73a866) #x0000000000000000))
(constraint (= (f #x00ec2513db6a72e7) #x00ec2513db6a72e7))
(constraint (= (f #x918bee85025becbe) #x0000000000000000))
(constraint (= (f #x00876967d1d88b9a) #x010ed2cfa3b11734))
(constraint (= (f #xed6e66e58345eae6) #x0000000000000000))
(constraint (= (f #xb9de06175ae5a7c7) #x73bc0c2eb5cb4f8e))
(constraint (= (f #x415b4860ee178b8a) #x82b690c1dc2f1714))
(constraint (= (f #x8c94866cac574243) #x19290cd958ae8486))
(constraint (= (f #x98db531deaeb1658) #x31b6a63bd5d62cb0))
(constraint (= (f #x10ce50a7e00307bd) #x0000000000000001))
(constraint (= (f #x9841e4e5783d44b8) #x0000000000000000))
(constraint (= (f #x74a2c54eebe3a136) #x0000000000000000))
(constraint (= (f #xa4ac27b4643cbc06) #x49584f68c879780c))
(check-synth)
(define-fun f_1 ((x (BitVec 64))) (BitVec 64) (ite (= (bvand #x0000000000000001 x) #x0000000000000000) (ite (= (bvurem x #x000000000000000a) #x0000000000000002) (ite (= (bvurem x #x0000000000000007) #x0000000000000002) (bvadd x x) (ite (= (bvand #x0000000000000003 x) #x0000000000000002) #x0000000000000000 (ite (= (bvurem x #x0000000000000006) #x0000000000000000) (ite (= (bvurem x #x0000000000000007) #x0000000000000001) (bvadd x x) #x0000000000000000) (bvadd x x)))) (ite (= (bvurem x #x000000000000000f) #x0000000000000000) (ite (= (bvor #x0000000000000010 x) x) #x0000000000000000 (ite (= (bvurem x #x0000000000000007) #x0000000000000003) x #x0000000000000000)) (ite (= (bvurem x #x000000000000000b) #x0000000000000001) x (ite (= (bvurem x #x0000000000000009) #x0000000000000001) (ite (= (bvurem x #x0000000000000007) #x0000000000000000) #x0000000000000000 (bvadd x x)) (ite (= (bvurem x #x000000000000000f) #x0000000000000001) (ite (= (bvor #x0000000000000010 x) x) x (ite (= (bvand #x0000000000000003 x) #x0000000000000002) x #x0000000000000000)) (ite (= (bvor #x000000000000000e x) x) (ite (= (bvor #x0000000000000010 x) x) (ite (= (bvurem x #x0000000000000006) #x0000000000000000) x (bvadd x x)) x) (ite (= (bvsrem x #x000000000000000c) #x0000000000000002) (ite (= (bvurem x #x0000000000000007) #x0000000000000001) (bvadd x x) x) (ite (= (bvurem x #x000000000000000d) #x0000000000000001) (ite (= (bvand #x0000000000000003 x) #x0000000000000002) (bvadd x x) x) (ite (= (bvurem x #x000000000000000b) #x0000000000000002) #x0000000000000000 (ite (= (bvsrem x #x0000000000000006) #x0000000000000000) (ite (= (bvurem x #x0000000000000009) #x0000000000000003) #x0000000000000000 (ite (= (bvor #x0000000000000010 x) x) (ite (= (bvurem x #x0000000000000005) #x0000000000000001) (bvadd x x) #x0000000000000000) (bvadd x x))) (bvadd x x))))))))))) (ite (= (bvurem x #x0000000000000009) #x0000000000000001) (ite (= (bvurem x #x0000000000000005) #x0000000000000000) (bvadd x x) (ite (= (bvurem x #x0000000000000007) #x0000000000000001) x #x0000000000000001)) (ite (= (bvand #x0000000000000005 x) #x0000000000000001) (ite (= (bvurem x #x000000000000000f) #x0000000000000001) x (ite (= (bvurem x #x000000000000000c) #x0000000000000003) (ite (= (bvashr x x) #x0000000000000000) (bvadd x x) (ite (= (bvurem x #x0000000000000007) #x0000000000000000) (bvadd x x) x)) (bvadd x x))) (ite (= (bvurem x #x0000000000000005) #x0000000000000002) (ite (= (bvor #x0000000000000010 x) x) #x0000000000000001 x) (ite (= (bvsrem x #x0000000000000005) #x0000000000000000) (bvadd x x) (ite (= (bvurem x #x0000000000000003) #x0000000000000000) (ite (= (bvurem x #x0000000000000005) #x0000000000000000) #x0000000000000001 (bvadd x x)) (ite (= (bvurem x #x0000000000000007) #x0000000000000002) (ite (= (bvashr x x) #x0000000000000000) #x0000000000000001 (bvadd x x)) x))))))))
